$\forall$${\it es}$:ES, $i$, $x$:Id, $P$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow\mathbb{P}$), ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$${\it ds}$($x$)?Top).
\\[0ex]es{-}update{-}iff(${\it es}$;$i$;$x$;${\it ds}$;$e$.$P$($e$);$s$.$f$($s$)) $\in$ $\mathbb{P}$